

LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c379180 c379179)) v (c c379180 c379179))


> hypdisj
=============================
Step 3

? (c c379180 c379179)

1. (ec c379180 c379179)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c379180 c379179)

1. (~ (c c379180 c379179))
2. (ec c379180 c379179)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c384309 c384308)) v (p c384309 c384308))


> hypdisj
=============================
Step 3

? (p c384309 c384308)

1. (pp c384309 c384308)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c384309 c384308)

1. (~ (p c384309 c384308))
2. (pp c384309 c384308)

> hyp


LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c389494 c389493)) v (pp c389494 c389493))


> hypdisj
=============================
Step 3

? (pp c389494 c389493)

1. (tpp c389494 c389493)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c389494 c389493)

1. (~ (pp c389494 c389493))
2. (tpp c389494 c389493)

> hyp


LEMMA

Non-tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((ntpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (ntpp c394735 c394734)) v (pp c394735 c394734))


> hypdisj
=============================
Step 3

? (pp c394735 c394734)

1. (ntpp c394735 c394734)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c394735 c394734)

1. (~ (pp c394735 c394734))
2. (ntpp c394735 c394734)

> hyp


LEMMA

Parthood lifts connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c400034 c400033)) v (~ (c c400032 c400034))) v (c c400032 c400033))


> hypdisj
=============================
Step 3

? (c c400032 c400033)

1. (c c400032 c400034)
2. (p c400034 c400033)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c400033)
|
|1. (~ (c c400032 c400033))
|2. (c c400032 c400034)
|3. (p c400034 c400033)
|
|> hyp
=============================
Step 5

? (c c400032 c400034)

1. (~ (c c400032 c400033))
2. (c c400032 c400034)
3. (p c400034 c400033)

> hyp


LEMMA

If x is disconnected from y and y is externally connected to z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (ec y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (dc c405489 c405488)) v (~ (ec c405488 c405487))) v (~ (p c405487 c405489)))


> hypdisj
=============================
Step 3

? (~ (p c405487 c405489))

1. (ec c405488 c405487)
2. (dc c405489 c405488)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var30 c405487)
|
|1. (p c405487 c405489)
|2. (ec c405488 c405487)
|3. (dc c405489 c405488)
|
|> ((c X Y) <-- (ec X Y))
|=============================
|Step 5
|
|? (ec Var30 c405487)
|
|1. (~ (c Var30 c405487))
|2. (p c405487 c405489)
|3. (ec c405488 c405487)
|4. (dc c405489 c405488)
|
|> hyp
=============================
Step 6

? (~ (c c405488 c405489))

1. (p c405487 c405489)
2. (ec c405488 c405487)
3. (dc c405489 c405488)

> ((~ (c Y X)) <-- (~ (c X Y)))
=============================
Step 7

? (~ (c c405489 c405488))

1. (c c405488 c405489)
2. (p c405487 c405489)
3. (ec c405488 c405487)
4. (dc c405489 c405488)

> ((~ (c X Y)) <-- (dc X Y))
=============================
Step 8

? (dc c405489 c405488)

1. (c c405489 c405488)
2. (c c405488 c405489)
3. (p c405487 c405489)
4. (ec c405488 c405487)
5. (dc c405489 c405488)

> hyp


LEMMA

Case split on whether x is connected to z; if not, then dc x z.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (ec y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (dc c411100 c411099)) v (~ (ec c411099 c411098))) v ((dc c411100 c411098) v (c c411100 c411098)))


> hypdisj
=============================
Step 3

? (c c411100 c411098)

1. (~ (dc c411100 c411098))
2. (ec c411099 c411098)
3. (dc c411100 c411099)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c411100 c411098))

1. (~ (c c411100 c411098))
2. (~ (dc c411100 c411098))
3. (ec c411099 c411098)
4. (dc c411100 c411099)

> hyp


LEMMA

If x is connected to z, split on overlap to get ec x z or o x z.
=============================
Step 1

? (all x (all y (all z ((((dc x y) & (ec y z)) & (c x z)) => ((ec x z) v (o x z))))))


> revsk
=============================
Step 2

? ((((~ (dc c416977 c416976)) v (~ (ec c416976 c416975))) v (~ (c c416977 c416975))) v ((ec c416977 c416975) v (o c416977 c416975)))


> hypdisj
=============================
Step 3

? (o c416977 c416975)

1. (~ (ec c416977 c416975))
2. (c c416977 c416975)
3. (ec c416976 c416975)
4. (dc c416977 c416976)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c416977 c416975)
|
|1. (~ (o c416977 c416975))
|2. (~ (ec c416977 c416975))
|3. (c c416977 c416975)
|4. (ec c416976 c416975)
|5. (dc c416977 c416976)
|
|> hyp
=============================
Step 5

? (~ (ec c416977 c416975))

1. (~ (o c416977 c416975))
2. (~ (ec c416977 c416975))
3. (c c416977 c416975)
4. (ec c416976 c416975)
5. (dc c416977 c416976)

> hyp


LEMMA

If x overlaps z and z is not part of x, then either po x z or pp x z.
=============================
Step 1

? (all x (all y (all z (((((dc x y) & (ec y z)) & (c x z)) & (o x z)) => ((po x z) v (pp x z))))))


> revsk
=============================
Step 2

? (((((~ (dc c423270 c423269)) v (~ (ec c423269 c423268))) v (~ (c c423270 c423268))) v (~ (o c423270 c423268))) v ((po c423270 c423268) v (pp c423270 c423268)))


> hypdisj
=============================
Step 3

? (pp c423270 c423268)

1. (~ (po c423270 c423268))
2. (o c423270 c423268)
3. (c c423270 c423268)
4. (ec c423269 c423268)
5. (dc c423270 c423269)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c423270 c423268)
|
|1. (~ (pp c423270 c423268))
|2. (~ (po c423270 c423268))
|3. (o c423270 c423268)
|4. (c c423270 c423268)
|5. (ec c423269 c423268)
|6. (dc c423270 c423269)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 5
||
||? (p c423268 c423270)
||
||1. (~ (p c423270 c423268))
||2. (~ (pp c423270 c423268))
||3. (~ (po c423270 c423268))
||4. (o c423270 c423268)
||5. (c c423270 c423268)
||6. (ec c423269 c423268)
||7. (dc c423270 c423269)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c423270 c423268)
||||
||||1. (~ (p c423268 c423270))
||||2. (~ (p c423270 c423268))
||||3. (~ (pp c423270 c423268))
||||4. (~ (po c423270 c423268))
||||5. (o c423270 c423268)
||||6. (c c423270 c423268)
||||7. (ec c423269 c423268)
||||8. (dc c423270 c423269)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (p c423270 c423268))
|||
|||1. (~ (p c423268 c423270))
|||2. (~ (p c423270 c423268))
|||3. (~ (pp c423270 c423268))
|||4. (~ (po c423270 c423268))
|||5. (o c423270 c423268)
|||6. (c c423270 c423268)
|||7. (ec c423269 c423268)
|||8. (dc c423270 c423269)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c423270 c423268))
||
||1. (~ (p c423268 c423270))
||2. (~ (p c423270 c423268))
||3. (~ (pp c423270 c423268))
||4. (~ (po c423270 c423268))
||5. (o c423270 c423268)
||6. (c c423270 c423268)
||7. (ec c423269 c423268)
||8. (dc c423270 c423269)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c423268 c423270))
|
|1. (~ (p c423270 c423268))
|2. (~ (pp c423270 c423268))
|3. (~ (po c423270 c423268))
|4. (o c423270 c423268)
|5. (c c423270 c423268)
|6. (ec c423269 c423268)
|7. (dc c423270 c423269)
|
|> ((~ (pp X Y)) <-- (~ (p X Y)))
|=============================
|Step 10
|
|? (~ (p c423268 c423270))
|
|1. (pp c423268 c423270)
|2. (~ (p c423270 c423268))
|3. (~ (pp c423270 c423268))
|4. (~ (po c423270 c423268))
|5. (o c423270 c423268)
|6. (c c423270 c423268)
|7. (ec c423269 c423268)
|8. (dc c423270 c423269)
|
|> ((~ (p Z X)) <-- (dc X Y) (ec Y Z))
||=============================
||Step 11
||
||? (dc c423270 Var51)
||
||1. (p c423268 c423270)
||2. (pp c423268 c423270)
||3. (~ (p c423270 c423268))
||4. (~ (pp c423270 c423268))
||5. (~ (po c423270 c423268))
||6. (o c423270 c423268)
||7. (c c423270 c423268)
||8. (ec c423269 c423268)
||9. (dc c423270 c423269)
||
||> hyp
|=============================
|Step 12
|
|? (ec c423269 c423268)
|
|1. (p c423268 c423270)
|2. (pp c423268 c423270)
|3. (~ (p c423270 c423268))
|4. (~ (pp c423270 c423268))
|5. (~ (po c423270 c423268))
|6. (o c423270 c423268)
|7. (c c423270 c423268)
|8. (ec c423269 c423268)
|9. (dc c423270 c423269)
|
|> hyp
=============================
Step 13

? (~ (p c423268 c423270))

1. (~ (pp c423270 c423268))
2. (~ (po c423270 c423268))
3. (o c423270 c423268)
4. (c c423270 c423268)
5. (ec c423269 c423268)
6. (dc c423270 c423269)

> ((~ (p Z X)) <-- (dc X Y) (ec Y Z))
|=============================
|Step 14
|
|? (dc c423270 Var56)
|
|1. (p c423268 c423270)
|2. (~ (pp c423270 c423268))
|3. (~ (po c423270 c423268))
|4. (o c423270 c423268)
|5. (c c423270 c423268)
|6. (ec c423269 c423268)
|7. (dc c423270 c423269)
|
|> hyp
=============================
Step 15

? (ec c423269 c423268)

1. (p c423268 c423270)
2. (~ (pp c423270 c423268))
3. (~ (po c423270 c423268))
4. (o c423270 c423268)
5. (c c423270 c423268)
6. (ec c423269 c423268)
7. (dc c423270 c423269)

> hyp


LEMMA

Proper part decomposes into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c430173 c430172)) v ((tpp c430173 c430172) v (ntpp c430173 c430172)))


> hypdisj
=============================
Step 3

? (ntpp c430173 c430172)

1. (~ (tpp c430173 c430172))
2. (pp c430173 c430172)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f423387 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c430173 c430172)
|
|1. (~ (ntpp c430173 c430172))
|2. (~ (tpp c430173 c430172))
|3. (pp c430173 c430172)
|
|> hyp
=============================
Step 5

? (~ (ec (f423387 c430173 c430172 Var32) c430173))

1. (~ (ntpp c430173 c430172))
2. (~ (tpp c430173 c430172))
3. (pp c430173 c430172)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c430173 Var36)
||
||1. (ec (f423387 c430173 c430172 Var32) c430173)
||2. (~ (ntpp c430173 c430172))
||3. (~ (tpp c430173 c430172))
||4. (pp c430173 c430172)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f423387 c430173 c430172 Var32) c430172)
|
|1. (ec (f423387 c430173 c430172 Var32) c430173)
|2. (~ (ntpp c430173 c430172))
|3. (~ (tpp c430173 c430172))
|4. (pp c430173 c430172)
|
|> ((ec (f423387 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c430173 c430172))
||
||1. (~ (ec (f423387 c430173 c430172 Var32) c430172))
||2. (ec (f423387 c430173 c430172 Var32) c430173)
||3. (~ (ntpp c430173 c430172))
||4. (~ (tpp c430173 c430172))
||5. (pp c430173 c430172)
||
||> hyp
|=============================
|Step 9
|
|? (pp c430173 c430172)
|
|1. (~ (ec (f423387 c430173 c430172 Var32) c430172))
|2. (ec (f423387 c430173 c430172 Var32) c430173)
|3. (~ (ntpp c430173 c430172))
|4. (~ (tpp c430173 c430172))
|5. (pp c430173 c430172)
|
|> hyp
=============================
Step 10

? (~ (tpp c430173 c430172))

1. (ec (f423387 c430173 c430172 Var32) c430173)
2. (~ (ntpp c430173 c430172))
3. (~ (tpp c430173 c430172))
4. (pp c430173 c430172)

> hyp


LEMMA

Refine the overlap case from po or pp to po or tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((((dc x y) & (ec y z)) & (c x z)) & (o x z)) => ((po x z) v ((tpp x z) v (ntpp x z)))))))


> revsk
=============================
Step 2

? (((((~ (dc c437229 c437228)) v (~ (ec c437228 c437227))) v (~ (c c437229 c437227))) v (~ (o c437229 c437227))) v ((po c437229 c437227) v ((tpp c437229 c437227) v (ntpp c437229 c437227))))


> hypdisj
=============================
Step 3

? (ntpp c437229 c437227)

1. (~ (tpp c437229 c437227))
2. (~ (po c437229 c437227))
3. (o c437229 c437227)
4. (c c437229 c437227)
5. (ec c437228 c437227)
6. (dc c437229 c437228)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c437229 c437227)
|
|1. (~ (ntpp c437229 c437227))
|2. (~ (tpp c437229 c437227))
|3. (~ (po c437229 c437227))
|4. (o c437229 c437227)
|5. (c c437229 c437227)
|6. (ec c437228 c437227)
|7. (dc c437229 c437228)
|
|> ((pp Y Z) <-- (dc Y X) (ec X Z) (c Y Z) (o Y Z) (~ (po Y Z)))
|||||=============================
|||||Step 5
|||||
|||||? (dc c437229 Var32)
|||||
|||||1. (~ (pp c437229 c437227))
|||||2. (~ (ntpp c437229 c437227))
|||||3. (~ (tpp c437229 c437227))
|||||4. (~ (po c437229 c437227))
|||||5. (o c437229 c437227)
|||||6. (c c437229 c437227)
|||||7. (ec c437228 c437227)
|||||8. (dc c437229 c437228)
|||||
|||||> hyp
||||=============================
||||Step 6
||||
||||? (ec c437228 c437227)
||||
||||1. (~ (pp c437229 c437227))
||||2. (~ (ntpp c437229 c437227))
||||3. (~ (tpp c437229 c437227))
||||4. (~ (po c437229 c437227))
||||5. (o c437229 c437227)
||||6. (c c437229 c437227)
||||7. (ec c437228 c437227)
||||8. (dc c437229 c437228)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (c c437229 c437227)
|||
|||1. (~ (pp c437229 c437227))
|||2. (~ (ntpp c437229 c437227))
|||3. (~ (tpp c437229 c437227))
|||4. (~ (po c437229 c437227))
|||5. (o c437229 c437227)
|||6. (c c437229 c437227)
|||7. (ec c437228 c437227)
|||8. (dc c437229 c437228)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c437229 c437227)
||
||1. (~ (pp c437229 c437227))
||2. (~ (ntpp c437229 c437227))
||3. (~ (tpp c437229 c437227))
||4. (~ (po c437229 c437227))
||5. (o c437229 c437227)
||6. (c c437229 c437227)
||7. (ec c437228 c437227)
||8. (dc c437229 c437228)
||
||> hyp
|=============================
|Step 9
|
|? (~ (po c437229 c437227))
|
|1. (~ (pp c437229 c437227))
|2. (~ (ntpp c437229 c437227))
|3. (~ (tpp c437229 c437227))
|4. (~ (po c437229 c437227))
|5. (o c437229 c437227)
|6. (c c437229 c437227)
|7. (ec c437228 c437227)
|8. (dc c437229 c437228)
|
|> hyp
=============================
Step 10

? (~ (tpp c437229 c437227))

1. (~ (ntpp c437229 c437227))
2. (~ (tpp c437229 c437227))
3. (~ (po c437229 c437227))
4. (o c437229 c437227)
5. (c c437229 c437227)
6. (ec c437228 c437227)
7. (dc c437229 c437228)

> hyp


LEMMA

Combine the three local case splits: dc or c; if c then ec or o; if o then po or pp; finally split pp into tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (ec y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (dc c445145 c445144)) v (~ (ec c445144 c445143))) v (((((dc c445145 c445143) v (ec c445145 c445143)) v (po c445145 c445143)) v (tpp c445145 c445143)) v (ntpp c445145 c445143)))


> hypdisj
=============================
Step 3

? (ntpp c445145 c445143)

1. (~ (tpp c445145 c445143))
2. (~ (po c445145 c445143))
3. (~ (ec c445145 c445143))
4. (~ (dc c445145 c445143))
5. (ec c445144 c445143)
6. (dc c445145 c445144)

> ((ntpp Y Z) <-- (dc Y X) (ec X Z) (c Y Z) (o Y Z) (~ (po Y Z)) (~ (tpp Y Z)))
|||||=============================
|||||Step 4
|||||
|||||? (dc c445145 Var35)
|||||
|||||1. (~ (ntpp c445145 c445143))
|||||2. (~ (tpp c445145 c445143))
|||||3. (~ (po c445145 c445143))
|||||4. (~ (ec c445145 c445143))
|||||5. (~ (dc c445145 c445143))
|||||6. (ec c445144 c445143)
|||||7. (dc c445145 c445144)
|||||
|||||> hyp
||||=============================
||||Step 5
||||
||||? (ec c445144 c445143)
||||
||||1. (~ (ntpp c445145 c445143))
||||2. (~ (tpp c445145 c445143))
||||3. (~ (po c445145 c445143))
||||4. (~ (ec c445145 c445143))
||||5. (~ (dc c445145 c445143))
||||6. (ec c445144 c445143)
||||7. (dc c445145 c445144)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (c c445145 c445143)
|||
|||1. (~ (ntpp c445145 c445143))
|||2. (~ (tpp c445145 c445143))
|||3. (~ (po c445145 c445143))
|||4. (~ (ec c445145 c445143))
|||5. (~ (dc c445145 c445143))
|||6. (ec c445144 c445143)
|||7. (dc c445145 c445144)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 7
|||
|||? (~ (dc c445145 c445143))
|||
|||1. (~ (c c445145 c445143))
|||2. (~ (ntpp c445145 c445143))
|||3. (~ (tpp c445145 c445143))
|||4. (~ (po c445145 c445143))
|||5. (~ (ec c445145 c445143))
|||6. (~ (dc c445145 c445143))
|||7. (ec c445144 c445143)
|||8. (dc c445145 c445144)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c445145 c445143)
||
||1. (~ (ntpp c445145 c445143))
||2. (~ (tpp c445145 c445143))
||3. (~ (po c445145 c445143))
||4. (~ (ec c445145 c445143))
||5. (~ (dc c445145 c445143))
||6. (ec c445144 c445143)
||7. (dc c445145 c445144)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 9
|||
|||? (c c445145 c445143)
|||
|||1. (~ (o c445145 c445143))
|||2. (~ (ntpp c445145 c445143))
|||3. (~ (tpp c445145 c445143))
|||4. (~ (po c445145 c445143))
|||5. (~ (ec c445145 c445143))
|||6. (~ (dc c445145 c445143))
|||7. (ec c445144 c445143)
|||8. (dc c445145 c445144)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 10
|||
|||? (~ (dc c445145 c445143))
|||
|||1. (~ (c c445145 c445143))
|||2. (~ (o c445145 c445143))
|||3. (~ (ntpp c445145 c445143))
|||4. (~ (tpp c445145 c445143))
|||5. (~ (po c445145 c445143))
|||6. (~ (ec c445145 c445143))
|||7. (~ (dc c445145 c445143))
|||8. (ec c445144 c445143)
|||9. (dc c445145 c445144)
|||
|||> hyp
||=============================
||Step 11
||
||? (~ (ec c445145 c445143))
||
||1. (~ (o c445145 c445143))
||2. (~ (ntpp c445145 c445143))
||3. (~ (tpp c445145 c445143))
||4. (~ (po c445145 c445143))
||5. (~ (ec c445145 c445143))
||6. (~ (dc c445145 c445143))
||7. (ec c445144 c445143)
||8. (dc c445145 c445144)
||
||> hyp
|=============================
|Step 12
|
|? (~ (po c445145 c445143))
|
|1. (~ (ntpp c445145 c445143))
|2. (~ (tpp c445145 c445143))
|3. (~ (po c445145 c445143))
|4. (~ (ec c445145 c445143))
|5. (~ (dc c445145 c445143))
|6. (ec c445144 c445143)
|7. (dc c445145 c445144)
|
|> hyp
=============================
Step 13

? (~ (tpp c445145 c445143))

1. (~ (ntpp c445145 c445143))
2. (~ (tpp c445145 c445143))
3. (~ (po c445145 c445143))
4. (~ (ec c445145 c445143))
5. (~ (dc c445145 c445143))
6. (ec c445144 c445143)
7. (dc c445145 c445144)

> hyp
